Inference at * 1 0 
Iof proof for Lemma linorder functionality wrt iff:



1. T : Type
2. R : TT
3. R' : TT
4. x, y:T. R(x,y)  R'(x,y)
  (Order(T;x,y.R(x,y)) & Connex(T;x,y.R(x,y)))
   (Order(T;x,y.R'(x,y)) & Connex(T;x,y.R'(x,y))) 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{2:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{7:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{7:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n} 

latex

 1: .....wf..... NILNIL

 1:   (Order(T;x,y.R(x,y)) & Connex(T;x,y.R(x,y)))  
 2: .....wf..... NILNIL

 2:   (Order(T;x,y.R'(x,y)) & Connex(T;x,y.R'(x,y)))  
 3: .....wf..... NILNIL

 3:   Order(T;x,y.R(x,y))  
 4: .....wf..... NILNIL

 4:   Order(T;x,y.R'(x,y))  
 5: .....wf..... NILNIL

 5:   Connex(T;x,y.R(x,y))  
 6: .....wf..... NILNIL

 6:   Connex(T;x,y.R'(x,y))  
 7: .....wf..... NILNIL

 7:   T  Type
 8: .....wf..... NILNIL

 8:   (x,y. R(x,y))  TT
 9: .....wf..... NILNIL

 9:   (x,y. R'(x,y))  TT
 10: .....wf..... NILNIL

 10: 5. x : T
 10: 6. T
 10:   x  T
 11: .....wf..... NILNIL

 11: 5. T
 11: 6. y : T
 11:   y  T
 12: .....wf..... NILNIL

 12: 5. T
 12:   T  Type
 13: .....wf..... NILNIL

 13:   (Order(T;x,y.R'(x,y)) & Connex(T;x,y.R'(x,y)))
 13:   =
 13:   (Order(T;x,y.R'(x,y)) & Connex(T;x,y.R'(x,y)))
 14: 

 14:   (Order(T;x,y.R'(x,y)) & Connex(T;x,y.R'(x,y)))
 14:    (Order(T;x,y.R'(x,y)) & Connex(T;x,y.R'(x,y)))
 .

Definitions	t  T, x:A  B(x), x.A(x), f(a), s = t, Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), , x:AB(x), Type, x(s1,s2), x,y. t(x;y), P  Q, P  Q, P & Q, P  Q, x:A. B(x)
Lemmas	connex functionality wrt iff, order functionality wrt iff, and functionality wrt iff, iff functionality wrt iff